%!TEX root = paperEdit.tex
\section{Worked Example}
\label{sec:example}

We have used REPROVE to automatically reverse-engineer the \func{C\_login} function in
five commercially available smart-cards. We had access to the implementation
of the APDU of each smart-card but we treated these implementations as
unknown for the purposes of our evaluation. In this section we demonstrate
the automated reverse-engineering procedure through an example. Because of a non-disclosure
agreement we cannot provide full details of the card implementation. We
explain each reverse-engineering step in detail and we provide an example of the applied
rules only for the first step. 
During the example we only refer to predicate names, to aid readability.


%30/4

\subsection{APDU trace}
Consider the following APDU trace for the  RSA PKCS\#11 \func{C\_login}
function:
\begin{compactenum}
	\item $\cmdvar{command}(\var{Cla}_1, \var{Ins}_1, \var{P1}_1, \var{P2}_1,
		\val{	00}, \val{00}, \val{null})$
	\item $\cmdvar{command}(\val{00}, \var{a4}, \val{P1}_2, \var{09},
		\var{Lc}_2, \var{D}_2, \val{null})$
	\item $\cmdvar{command}(\var{Cla}_3, \var{Ins}_3, \var{P1}_3, \var{P2}_3, 
		\val{00}, \val{00}, \var{Le}_3)$
	\item $\cmdvar{command}(\var{Cla}_4, \var{Ins}_4, \var{P1}_4, \var{P2}_4, 
		\var{Lc}_4, \val{D}_4, \val{null})$
	\item $\cmdvar{command}(\val{00}, \val{a4}, \var{P1}_5, \var{P2}_5, \val{00},
	\val{00}, \val{00})$
\end{compactenum}
\noindent where all values are given as hexadecimal numbers.  Though the
trace is actually a stream of bytes, we have split these bytes at appropriate
intervals to delimit full commands.  Each such command will be analyzed by
REPROVE in order to be matched to inter-industry commands.  Subsequently,
commands will then be grouped into different (sub-)/functionalities for the
purpose of deciphering the full semantics of the communication.

\begin{compactenum}[Step 1.]
\item The trace suggests that there two
commands (2 and 5) that are inter-industry commands since they have a value
for the \var{Cla} field equal to \val{00}.  There are also three
proprietary commands: 1, 3 and 4.  For these three commands, their
corresponding classifications are unknown and are initialized as variables
$\var{Cla}_1$, $\var{Cla}_3$ and $\var{Cla}_4$. REPROVE will first produce 
mappings from the inter-industry commands to sub-functionalities and functionalities, 
if possible. Then, REPROVE will assign proprietary commands to the
corresponding category by looking at their data exchange properties.   To
employ these processes, the system applies the following rules:
\begin{compactenum}[1)]
\item $ \lefteqn{\forall     \var{P1}, \var{Lc}, \var{D} ( }\\ 
				\lefteqn{\cmdvar{command}(\val{00}, \val{a4}, \var{P1}, \val{09}, 
					\var{Lc}, \var{D}, \val{null}) }\\
				~~~~\rightarrow \sfnclty{selected}(\val{path}, \var{D})) $
\item $ \lefteqn{\forall     \var{Cla}, \var{Ins}, \var{P1}, \var{P2} ( }\\ 
				\lefteqn{\cmdvar{command}(\var{Cla}, \var{Ins}, \var{P1}, \var{P2}, 
					\val{00}, \val{00}, \val{null}) }\\
				~~~~\rightarrow \cmdvar{command}_{nn}(\var{Cla}, \var{Ins}, \var{P1}, 
					\var{P2}, \val{00}, \val{00}, \val{null})) $
\item $ \lefteqn{\forall     \var{Cla}, \var{Ins}, \var{P1}, \var{P2},
					\var{Lc}, \var{D}, \var{Le} ( }\\ 
				\lefteqn{(\cmdvar{command}(\var{Cla}, \var{Ins}, \var{P1}, \var{P2}, 
					\val{00}, \val{00}, \var{Le}) }\\
				\lefteqn{\land\var{Le}\neq\val{null})}\\
				~~~~\rightarrow \cmdvar{command}_{ny}(\var{Cla}, \var{Ins}, \var{P1}, 
					\var{P2}, \val{00}, \val{00}, \var{Le})) $
\item $ \lefteqn{\forall     \var{Cla}, \var{Ins}, \var{P1}, \var{P2}, \var{Lc},
					\var{D} ( }\\ 
				\lefteqn{(\cmdvar{command}(\var{Cla}, \var{Ins}, \var{P1}, \var{P2}, 
					\var{Lc}, \var{D}, \val{null}) }\\
					\lefteqn{\land \var{Lc}\neq\val{00} \land
						\var{D}\neq\val{00})}\\
				~~~~\rightarrow \cmdvar{command}_{yn}(\var{Cla}, \var{Ins}, \var{P1}, 
					\var{P2}, \var{Lc}, \var{D}, \val{null}))	$
\end{compactenum}
\end{compactenum}



\eat{
\begin{eqnarray*}
1) \lefteqn{\forall     P1, Lc, D ( }\\ 
				\lefteqn{command(00, a4, P1, 09, Lc, D, null) }\\
				& \rightarrow selected(path, D))\\
2)   \lefteqn{\forall     Cla, Ins, P1, P2 ( }\\ 
				\lefteqn{command(Cla, Ins, P1, P2, 00, 00, null) }\\
				& \rightarrow command_{nn}(Cla, Ins, P1, P2, 00, 00, null))\\
3)  \lefteqn{\forall     Cla, Ins, P1, P2, Lc, D,Le ( }\\ 
				\lefteqn{(command(Cla, Ins, P1, P2, 00, 00, Le) }\\
				\lefteqn{\land Le\neq null)}\\
				& \rightarrow command_{ny}(Cla, Ins, P1, P2, 00, 00, Le))\\
4)   \lefteqn{\forall     Cla, Ins, P1, P2, Lc, D ( }\\ 
				\lefteqn{(command(Cla, Ins, P1, P2, Lc, D, null) }\\
				\lefteqn{\land Lc \neq 00 \land D \neq 00)}\\
				& \rightarrow command_{yn}(Cla, Ins, P1, P2, Lc, D, null))	
\end{eqnarray*}
}

The output of this step is the following model:
\begin{dmath*}
\cmdvar{command}_{nn}(\var{Cla}_1, \var{Ins}_1, \var{P1}_1, \var{P2}_1,
		\val{00}, \val{00}, \val{null}) \land 
	\sfnclty{selected}(\val{path}, \val{D}_2) \land 
	\cmdvar{command}_{ny}(\var{Cla}_3, \var{Ins}_3, \var{P1}_3, \var{P2}_3, 
		\val{00}, \val{00}, \var{Le}_3) \land 
	\cmdvar{command}_{yn}(\var{Cla}_4, \var{Ins}_4, \var{P1}_4, \var{P2}_4, 
		\var{Lc}_4, \val{d}_{4}) \land \fnclty{dummy}
\end{dmath*}

Recall that the predicate $\cmdvar{command}_{nn}$ conveys that no data is
sent and no data is expected; $\cmdvar{command}_{ny}$ implies that no data is
sent, but data is expected; $\cmdvar{command}_{yn}$ means that data is sent,
but no data is expected; and $\fnclty{dummy}$ is a special 
 placeholder for all commands that do nothing and cannot be further analyzed. For instance, the last
inter-industry command is a \cmd{select} command that simply queries the
card and it does not affect the analysis of the commands that follow. Thus, it is mapped to $\fnclty{dummy}$.

The reverse-engineering of the remaining trace (\ie the proprietary commands) is
sequential. We begin from the first proprietary command, and continue until
the last one.  Each proprietary command is referred to by its $\var{Ins}$
field.

\subsubsection{Analysis of $\val{Ins}_1$} This is the analysis of the first
proprietary command found in the trace.  For each such command we apply 
the remaining steps of our reverse-engineering process.

\begin{compactenum}[Step 1.]
\setcounter{enumi}{1}
	\item The set of command mappings, based on the category the command
	belongs to ($\cmdvar{command}_{nn}$) is:\\ $\{ \cmd{select}, \cmd{verify},
	\cmd{external\_authenticate}\}$.
 \item  The set of command mappings is refined based on precondition
 satisfiability:
  \begin{compactitem} 
		\item  $\cmd{select}$ is discarded as there is already an interindustry implementation of that command within the trace. 
		\item  $\cmd{verify}$ is valid, but it does not require any data back
		from the card. It is only used to check whether verification is required.
		So, it does not affect the commands that follow.
		\item  $\cmd{external\_authenticate}$:  the empty body of this command
		has the same meaning as in the \cmd{verify} command.
	\end{compactitem}
\end{compactenum}
\noindent The set of valid mappings, as extracted by the previous steps, is
therefore $\{$\cmd{verify},
\cmd{external\_authenticate}$\}$. As neither command affects the analysis of
the later commands the proprietary command is mapped to $\fnclty{dummy}$.  At
this point we can stop further analyzing the command as we know it cannot be
refined more.


\subsubsection{Analysis of $\var{Ins}_3$} Our analysis follows the same
principles as the one for $\var{Ins}_1$, though, as we will see, it performs
more reverse-engineering steps.

\begin{compactenum}[Step 1.]
\setcounter{enumi}{1}
	\item The set of command mappings for $\var{Ins}_{3}$, based on the
		category is belongs to ($\cmdvar{command}_{ny}$) is:\\
		 $\{ $\cmd{select},
		\cmd{read\_binary}, \cmd{get\_challenge}, \\ \cmd{read\_record}, 
		\cmd{get\_response}, \cmd{get\_data}$\}$.

	\item  The set of command mappings is refined based on precondition
	satisfiability:
 		\begin{compactitem} 
			\item  $\cmd{select}$ is  discarded as we know that the card
				implements this command in an inter-industry way.
			\item  $\cmd{read\_binary}$ is discarded as the precondition 
				$\sfnclty{selected}(\val{file}, \var{EF})$ is not satisfied.
			\item  $\cmd{get\_challenge}$  is  valid as it does not have any
				special preconditions.
			\item  $\cmd{read\_record}$ is discarded as
				$\sfnclty{selected}(\val{file}, \var{EF})$ is not satisfied.
			\item  $\cmd{get\_response}$ is valid as it does not have any special
				preconditions.
			\item  $\cmd{get\_data}$ is discarded as 
				$\sfnclty{selected}(\val{file}, \var{EF})$  is not satisfied.
		\end{compactitem} 
	Thus, the set of valid mappings is:\\
	 $\{$\cmd{get\_challenge}, \cmd{get\_response}$\}$.

	\item All possible partially/satisfiable (sub-)/functionalities are found.
		The outcome of this process is:
		\begin{compactitem}
			\item  $\sfnclty{challenge\_sent}(\var{Le}_3, \var{Challenge})$ 
				which is satisfied by the model: 
$\sfnclty{selected}$ $(\val{path},$
				$\var{D}_2)$ $\land$
                                $\sfnclty{get\_challenge}$ $(\var{Le}_3,$
				$\var{Challenge})$.
			\item $\sfnclty{get\_response}(\var{Le}_3, \var{RD})$ which is
			satisfied by the model:  $\sfnclty{selected}$ $(\val{path},$ $\var{D}_2)$
			$\land$ $\sfnclty{get\_response}$ $(\var{Le}_3,$
			$\var{RD})$.\footnote{$\sfnclty{selected}(\val{path}, \var{DF})$
			is an additional sub-functionality here. The model is
			satisfiable with or without it.}
		\end{compactitem}
\end{compactenum}

%%%edo-30/4
\subsubsection{Analysis of $\var{Ins}_4$, case 1: $\sfnclty{selected}(\val{path},
				\var{D}_2)$ $\land$ $\sfnclty{get\_challenge}(\var{Le}_3,
				\var{Challenge})$ for $\var{Ins}_3$} This corresponds to the first
				case for the potential mapping of the previous command.


\begin{compactenum}[Step 1.]
\setcounter{enumi}{1}
	\item The set of command mappings for $\var{Ins}_4$ based on the category it
		belongs to ( $\cmdvar{command}_{yn}$) is:\\ 
		$\{$\cmd{select},
		\cmd{create\_file}, \cmd{update\_binary}, \\ \cmd{external\_authenticate},
		\cmd{write\_record}, \\ \cmd{append\_record}, \cmd{update\_record}, 
		\cmd{put\_data}$\}$.

	\item The set of command mappings is refined  based on precondition
		satisfiability:
		\begin{compactitem} 
			\item $\cmd{select}$ is  discarded as we know, from the trace, the card implements this
				command in an inter-industry way.
			\item $\cmd{create\_file}$ is valid as
                          $\sfnclty{selected}$ $(\val{path},$
				$\val{EF})$ is satisfied.
			\item $\cmd{update\_binary}$ is discarded as
                          $\sfnclty{selected}$ $(\val{file},$
				$\var{EF})$ is not satisfied.
			\item $\cmd{external\_authenticate}$ is valid
                          as \\ 
				$\sfnclty{challenge\_sent}$ $(\var{Le},$ $\var{Challenge})$ is satisfied.
			\item $\cmd{write\_record}$ is discarded as $\sfnclty{selected}(\val{file},
				\var{EF})$  is not satisfied.
			\item $\cmd{append\_record}$ is discarded as
                          $\sfnclty{selected}$ $(\val{file},$
				$\var{EF})$  is not satisfied.
			\item $\cmd{update$\_$record}$ is discarded as
                           $\sfnclty{selected}$ $(\val{file},$
				$\var{EF})$ is not satisfied.
			\item $\cmd{put\_data}$ is discarded as $\sfnclty{selected}(\val{file},
				\var{EF})$ is not satisfied.
		\end{compactitem} 
		The set of valid mappings is:\\
		 $\{$\cmd{create\_file},
		\cmd{external\_authenticate}$\}$.

	\item All possible partially/satisfiable (sub-)/functionalities are found.
		The outcome of this process is:
		\begin{compactitem}
			\item $\sfnclty{file\_created}(\var{D}_2, \var{D}_4)$, which is
				satisfiable by the model: $\sfnclty{selected}(\val{path}, \var{D}_2)$
				$\land$ $\sfnclty{create\_file}(\var{D}_4)$,\\ \eat{\\with the
				following mappings:
					\begin{itemize}
						\item $DF \mapsto d_{2}$
						\item $D \mapsto d_{4}$
					\end{itemize}
				}
				and $\sfnclty{file\_created}(\var{D}_2, \var{D}_4) \mapsto $ $\fnclty{store\_data}(
				\var{D}_2, \var{D}_4)$.
%\\ which maps to  $store\_data(d_{2}, d_{4})$ \normalsize with the same argument instantiation as before.		

			\item $\sfnclty{external\_authenticated}(\var{Challenge}, \var{D}_4)$ 
				which is satisfiable by the models: 
					\begin{compactenum}[(\itshape i\upshape)]
						\item $\sfnclty{selected}(\val{path}, \var{D}_2)$
							$\land \cmd{get\_challenge}(\var{Le}_{3}, \var{Challenge})$ 
							$\land \cmd{external\_authenticate}(\var{D}_4)$,
							\eat{\\with the following mappings: 
								\begin{itemize}
									\item $Challenge \mapsto RD$
									\item $Response \mapsto d_{4}$
								\end{itemize}}
						\item $\sfnclty{selected}(\val{path}, \var{D}_2)$
							$\land \cmd{get\_response}(\var{Le}_3, \var{Challenge})$
							$\land \cmd{external\_authenticate}(\var{D}_4)$\footnote{$\sfnclty{selected}(
							\val{path}, \var{D}_2$) is an additional sub-functionality
							here. The model is satisfiable with or without it.}
					\end{compactenum}
					\noindent and $\sfnclty{external\_authenticated}(\var{Challenge},
						\var{D}_4)$ $\mapsto$
                                                \\ $\fnclty{authenticated}(\var{Challenge},
						\var{D}_4)$.

			\item  $\sfnclty{read\_data\_sub}(\val{card}, \var{Le}_4, \var{RD})$ 
				which is satisfiable by the model: $\cmd{get\_response}(\var{Le}_4, \var{RD})$. 
				\eat{with the following mappings:
					\begin{itemize}
						\item $Le \mapsto le_{4} $
						\item $D \mapsto RD$
					\end{itemize}	}			 
		\end{compactitem}
%%enty
	\item The \func{C\_login} models are matched  with the inferred ones.
		$\sfnclty{store\_data}(\var{D}_2, \var{D}_4)$ is discarded as  it does
		not match with any of \func{C\_login} models (the communication has ended
		and the authentication process is not satisfied).
		$\sfnclty{read\_data\_sub}(\val{card}, \var{Le}, \var{RD})$ is also
		discarded for the same reason. The only matching  model  is:
		$\fnclty{dummy}$ $\land$ $\sfnclty{selected}(\val{path}, \var{D}_2)$
		$\land$ $\fnclty{authenticated}(RD, \var{D}_4)$ $\land$ $\fnclty{dummy}$.
\end{compactenum}


\subsubsection{Analysis of $\var{Ins}_4$, case 2:
$\sfnclty{selected}(\val{path}, \var{D}_2)$ $\land$
$\cmd{get\_response}(\var{Le}_3, \var{RD})$ for $\var{Ins}_3$}

\begin{compactenum}
\setcounter{enumi}{1}
	\item The set of command mappings for $\var{Ins}_4$ based on the category
		it belongs to ($\cmdvar{command}_{yn}$) is:\\
		 $\{$\cmd{select}, \cmd{create\_file},
		\cmd{update\_binary}, \\ \cmd{external\_authenticate},
                \cmd{write\_record}, \\
		\cmd{append\_record}, \cmd{update\_record},  \cmd{put\_data}$\}$.

	\item The set of command mappings is refined  based on precondition
	satisfiability:
		\begin{compactitem} 
			\item $\cmd{select}$ is discarded as we know the card implements this
				command in an inter-industry way.
			\item $\cmd{create\_file}$ is valid as $\sfnclty{selected}(\var{path},
				\val{F})$ is satisfied.
			\item $\cmd{update\_binary}$ is discarded as $\sfnclty{selected}(\val{file},
				\var{EF})$  is not satisfied.
			\item $\cmd{external\_authenticate}$ is valid as
				$\sfnclty{challenge\_sent}$ $(\var{Le},$ $\var{Challenge})$  is satisfied.
			\item $\cmd{write\_record}$ is  discarded as
				$\sfnclty{selected}(\val{file}, \var{EF})$ is not satisfied.
			\item $\cmd{append\_record}$ is discarded as
				$\sfnclty{selected}(\val{file}, \var{EF})$ is not satisfied.
			\item $\cmd{update\_record}$ is discarded as
				$\sfnclty{selected}(\val{file}, \var{EF})$ is not satisfied.
			\item $\cmd{put\_data}$ is discarded as $\sfnclty{selected}(\val{file},
				\var{EF})$ is not satisfied.
		\end{compactitem} 
	The set of valid mappings is: \\
	 $\{$\cmd{create\_file},
		\cmd{external\_authenticate}$\}$.

	\item All possible  partially/satisfiable (sub-)/functionalities are found.
	The outcome of this process is:
		\begin{compactitem}
			\item  $\sfnclty{file\_created}(\var{D}_2, \var{D}_4)$ which is satisfiable
			by the model $\sfnclty{selected}(\val{path}, \var{D}_2)$ $\land$ 
			$\cmd{create\_file}(\val{D}_4)$
			\eat{ with the following mappings:
				\begin{itemize}
					\item  $df \mapsto to d_{2} $
					\item $D \mapsto d_{4}$
				\end{itemize}}
	 		and $\sfnclty{file\_created}(\var{D}_2, \var{D}_4) \mapsto 
	 			\fnclty{store\_data}(\var{D}_2, \var{D}_4)$.
%	  which is a sub-functionality of  $store\_data(d_{2}, d_{4})$  \normalsize with the same mappings as before.

			\item $\sfnclty{external\_authenticated}(\var{Challenge}, \var{D}_4)$
			 is discarded as it is satisfied by the model $\cmd{external\_authenticate}(
			 \var{D}_4)$ \normalsize  but  misses
			 the precondition $\sfnclty{challenge\_sent}(\var{Le},
			 \var{Challenge})$. 
		\end{compactitem}
  
%%%EDO

	\item The \func{C\_login} models are matched with the inferred ones.
	The model $\fnclty{store\_data}(\var{D}_2, \var{D}_4)$ is discarded as it
	does not match with any of the \func{C\_login} models (the communication
	has ended  without any authentication).
\end{compactenum} 

To conclude, the reverse-engineering process suggested  that \func{C\_login} is implemented as:
\begin{dmath*}
 \fnclty{dummy} \land \sfnclty{selected}(\val{path}, \var{D}_2) \land
 \fnclty{authenticated}(\var{Challenge}, \var{D}_4) \land \fnclty{dummy}
\end{dmath*}
\noindent which matches exactly with the actual implementation.





%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "paperEdit"
%%% End: 
